COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.REQUIRE "LSPMAC.PUB[LSP,CLT]" source_file
C00003 00003	.hd206 SPRING 1978
C00006 ENDMK
C⊗;
.REQUIRE "LSPMAC.PUB[LSP,CLT]" source_file;
.PAGE FRAME 56 HIGH 80 WIDE;
.evenleftborder ← oddleftborder ← 1000;
.area text lines 1 to 56;
.place text;
.
.MACRO  hd206 (TERM) ⊂
.BEGIN    NOFILL  TURNON "←→"
←COMPUTER SCIENCE DEPARTMENT
←STANFORD UNIVERSITY
.SKIP  
CS206  ←COMPUTING WITH SYMBOLIC EXPRESSIONS  →TERM
.TURNOFF
.END ⊃
.
.
.MACRO hw (NUMBER, DUEDATE) ⊂
.   BEGIN TURNON "←"  NOFILL
←PROBLEM SET  NUMBER
←Due  DUEDATE
.   TURNOFF END ⊃
.
.itemmac 1
.
.PORTION MAINPORTION
.
.hd206 SPRING 1978
.skip
.hw 2, |May 16|
.
.bb General comments. 


	This assignment involves proving properties of LISP functions.  
Unless otherwise noted your proofs should be fairly formal.  
The level of detail should be approximately
that of Chapter_III section_7 of the notes.  
For each step of your proof, make sure that 
you list all of the facts (axioms, earlier steps or previously proved properties)
that are necessary to make that step.  
You may use any facts already proved in the notes or in class.

.item←0
.begin   indent 0,6
.bb Assignment.

#. Chapter III.  Exercise 1. ii-v.

#. Chapter III.  Exercise 2. 

#. EXTRA (for practice with extended truth values, not required).
Let ⊗andlist be as defined in Chapter I and assume ⊗p is a suitably well-behaved
predicate.  Prove the following:

	##. ⊗⊗∀u v: [andlis[u*v, p] = andlis[u, p] ∧ andlis[v, p]]⊗

	##. ⊗⊗∀u: [andlis[reverse u, p] = andlis[u, p]]⊗

Hint: define ⊗aandlis, which returns an extended truth value corresponding to
the truth value of ⊗andlis on corresponding arguments.  Show that ⊗andlis
as defined in terms of ⊗aandlis satisfies the desired equivalence.  Then
you may use this result to prove other facts about ⊗andlis.  
The statement that "⊗p is suitably well-behaved" is rather vague.  You will
need to make it more precise in order to make your proof clear.   State this
 in your proof.
.end